Nuprl Lemma : swap_select
4,23
postcript
pdf
T
:Type,
L
:
T
List,
i
,
j
,
x
:
||
L
||. swap(
L
;
i
;
j
)[
x
] =
L
[(
i
,
j
)(
x
)]
T
latex
Definitions
x
:
A
.
B
(
x
)
,
i
j
,
||
as
||
,
(
i
,
j
)
,
{
i
..
j
}
,
t
T
,
P
Q
,
l
[
i
]
,
False
,
A
,
P
&
Q
,
A
B
,
i
j
<
k
,
,
P
Q
,
P
Q
,
swap(
L
;
i
;
j
)
Lemmas
int
seg
wf
,
permute
list
select
,
flip
wf
,
length
wf1
,
select
wf
,
non
neg
length
origin
T:Type, L:T List, i, j, x:
||L||. swap(L;i;j)[x] = L[(i, j)(x)] 
T T:Type, L:T List, i, j, x:||L||. swap(L;i;j)[x] = L[(i, j)(x)] T x:A. B(x)
j
} T
Q
A
B j < k
Q Q